Nuprl Lemma : component-realizes_wf 11,40
ds:(IdType{i}), da:(IdKndType{i}), A, B:Type{i}, C:component{i:l}(ds; da; A; B),
P:es-component{i:l}
P:es-component(A; B).
component-realizes{i:l}(ds; da; A; B; C; es,in,out.P(es,in,out))  {i''} 
latex

Definitionsx. t(x), P  Q, x(s1,s2,s3), C |- es,in,out.P(es;in;out), , t  T, x:A. B(x), x(s), ComponentSpec(A;B), Component(ds;da;A;B)
LemmasKnd wf, Id wf, component wf, es-component wf, event system wf, abs-interface wf, es-decl wf, scheme-realizes wf, interface wf

origin